\begin{tabbing}
chain\_config\_ind($x$;${\it head}$;${\it tail}$;${\it id}$.${\it pred}$(${\it id}$);${\it id}$,${\it num}$.${\it succ}$(${\it id}$;${\it num}$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it head}$\+
\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it tail}$\+
\\[0ex]$\mid$ inr($x$) =$>$ case $x$ of inl($x$) =$>$ ${\it pred}$($x$) $\mid$ inr($x$) =$>$ ${\it succ}$($x$.1;$x$.2)
\-\-\-\-
\end{tabbing}